Inference at * 1 1 1 
Iof proof for Lemma absval eq:



1. x : 
2. y : 
3. 0  x
4. 0  y
  (x = y)  x =  y 

latex

 by ((((((Unfold `pm_equal` 0) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 2:n
C),(first_nat 3:n)) (first_tok SupInf:t) inil_term)))) 
CollapseTHEN (Try (D (-1))))) 

CoCollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 1000:n)) (first_tok :t
C) inil_term))) 

latex

C.

Definitions

, t  T, P  Q, P  Q, P & Q, P  Q, i =  j, P  Q